Integrated circuits (ICs) have become the backbone of modern consumer electronics. The increased demand for functionality of consumer electronics has forced the complexity of IC's to skyrocket. In a number of applications, ICs must be highly functional, low cost and have low power consumption. These demands create increased complexity on the design, verification, and manufacture of ICs.
A typical IC design may involve the creation of electronic components, such as transistors and resistors, and the interconnections of these components onto a substrate, such as silicon. The simulation, verification, and sometimes layout of these components usually is accomplished in sub-blocks, or modules. Each block may be simulated and verified individually. Multiple design teams typically work on the individual blocks. During the design process functional verification is critical.
Functional verification involves the verification that the design conforms to the specification. Functional verification may involve the validation that a design meets the desired functionality. Part of the process of verification includes the creation of Register Transfer Level (RTL) digital designs that describe in detail the functionality of the device or block at every cycle of the clock. Creation and verification RTL design may be one of the more difficult portions of the design process. In many instances, this verification is a very difficult and time intensive task. Simulation tools are typically used to assist in verification.
Assertion-Based Verification (ABV) has been recently identified as a powerful verification paradigm that assures improved observability and controllability of the design, improved verification efficiency by detecting more bugs quickly and thereby facilitating enhanced productivity and higher design quality. With ABV, assertions are used to capture the required design behavior in an unambiguous way and constraints are used to define the environment for the assertion verification. Whenever an assertion fails, the tool displays a waveform that shows the sequence of events that has lead to the failure of assertion. On the other hand, when the answer to the correctness query is positive, most model-checking tools provide no additional information. In the last few years there has been growing awareness to the importance of suspecting the specification of environment for verification also in case model checking succeeds. The goal of vacuity check is to detect such incorrect environment specification (or over constraining) by further automatic reasoning even before we start assertion verification. The vacuity check detects if the constraints are in conflict with the design and also detects if the constraints are in conflict themselves. The challenge is to define vacuity check formally, develop algorithms for detecting the vacuous specification and most importantly report back the constraint or a list of constraints which are responsible for the vacuity.
Following approaches have been used in the past to handle such error situations.                Generate automatic trigger checks for the assertions. The trigger checks detect the coverage of a sequence of events associated with the assertion specification.        Perform vacuity checks to see if the constraints are in conflict with the design and also check to see if constraints are in conflict themselves without design specification.        
One problem with trigger checks is that they are part of the assertions and they can only check the coverage of trigger checks specific to one assertion. This can result in performance issues. Additionally, these checks do not provide any information up-front about the error in environment specification in an automatic way.
Vacuity checks, on the other hand, work on the constraints to check for valid environment specification. There are existing solutions and implementations to detect vacuity, but these implementations rely on particular model-checking techniques and may not work with different kinds of model checking engines (For example BDD based engines, SAT based engines or ATPG based engines).
Therefore, there exists a need for a system, and methods for detecting vacuity conditions.